$\forall$${\it es}$:ES. es\_val(${\it es}$) $\in$ $e$:E$\rightarrow$kindcase(kind($e$); $a$.es{-}V(${\it es}$)(loc($e$),$a$); $l$,$t$.es{-}M(${\it es}$)($l$,$t$) )